
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basics/relations.ma".
include "basics/logic.ma".
(*include "logic/coimplication.ma".*)

(* definition of a =_ID b. What is "break"? *)
notation "hvbox(a break = \sub \ID b)" 
  non associative with precedence 45 
  for @{ 'eqID $a $b }.

(* LR: Which is the difference with the notation just defined here above? 
       Doesn't the above notation become useless after the following one?
   CSC: "notation" is a notation used both in input and in output;
        "notation >" is used only in input. It is also given since it is
        more compact to write *)
notation > "hvbox(a break =_\ID b)" 
  non associative with precedence 45 
  for @{ cic:/matita/logic/eq.ind#xpointer(1/1) ? $a $b }.

(* Association of the notation a =_ID b to Leibniz equivalence 
   "cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b" ? *)
interpretation "ID eq" 'eqID x y = 
  (eq ? x y).

(* An arbitrary equivalence relation is a relation on a type A which is
   refl, sym, trans *)
record equivalence_relation (A:Type[0]) : Type[0] ≝
 { eq_rel:2> A → A → Prop;
   refl: reflexive ? eq_rel;
   sym: symmetric ? eq_rel;
   trans: transitive ? eq_rel
 }.

(* A setoid is weaker than a set meaning that it is based on a generic
   equivalence relation which is not necessarily Leibnitz relation *)
record setoid : Type[1] ≝
 { carr:> Type[0];
   eq: equivalence_relation carr
 }.

(* LR: Definition of a = b to denote the equivalence relation on a setoid.
       a = b stands for
       ????????????????
       I cannot read the meaning of  "eq_rel ? (eq ?) $a $b".
       "eq" should be defined in "setoid" and
       "eq_rel" in "equivalence_relation". 
       If this is true I cannot justify why "eq_rel" can have 4 arguments.
   CSC: Take the setoid
           S := { carr = T; eq = { eq_rel = # : T -> T -> Prop; ... }}
        a = b  stands for  (eq_rel ? (eq ?) a b)
        which is understood as (eq_rel T (eq S) a b) where a,b:T.

        eq_rel has four arguments since its type is:
           ∀ A:Type. setoid A → A → A → Prop
        in general all projections of a record are also quantified over the
        parameters of the record (here A) and the record itself (here"setoid A)"
*)
notation > "hvbox(a break = b)" 
  non associative with precedence 45 
  for @{ eq_rel ? (eq ?) $a $b }.
interpretation "eq setoid"
   'eq t x y = (eq_rel ? (eq t) x y). (* eq ?: ? → ? → Prop*)
interpretation "setoid symmetry" 
   'invert r = (sym ???? r). (* *)
     
(* LR: Why is .= linked to "trans"?
   CSC: Suppose your goal is a=b and 
        suppose you want to prove your goal using a lemma that
        proves a = a' to obtain a new goal a' = b 
        (i.e. you want to rewrite in the l.h.s. of the equation).
        
        This is possible since = is transitive, i.e.
        trans: ∀A.(setoid A) → (∀a,a',b. a=a' → a'=b → a=b)

        Hence, to perform the rewriting using the lemma r: a=a' it is
        sufficient to apply  (trans ????? r ?)  (the last question mark is
        added automatically by apply and it is the goal that remains open).
*)
notation ".= r" 
   with precedence 50 
   for @{'trans $r}.
interpretation "trans" 
  'trans r = (trans ????? r).

(* Notations associated to binary_morphism which ensures
   a function fun1: A → B is a morphism w.r.t. the equivalence
   relation eq *)
record unary_morphism (A,B: setoid) : Type[1] ≝
 { fun1:1> A → B;
   prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
 }.
(* Notation † c associated to the whole prop1 where c is a
   Prop, namely a statement that establishes the equality 
   between two elements of the (carrier) of a setoid *)
notation "† c" 
   with precedence 90 for @{'prop1 $c }. 
interpretation "prop1" 
   'prop1 c  = (prop1 ????? c).
(* Notation B:setoid ⇒ C:setoid associated to 
   the whole structure unary_morphism *)
notation "B ⇒ C" right associative 
   with precedence 72 
   for @{'unary_morphism $B $C}.
interpretation "'unary_morphism" 
   'unary_morphism A B = (unary_morphism A B).

(* Notations associated to binary_morphism which ensures
   a function fun2: A → B → C is a morphism w.r.t. the equivalence
   relation eq *)
record binary_morphism (A,B,C:setoid) : Type[1] ≝
 { fun2:2> A → B → C;
   prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
 }.
(* Notation l ‡ r  associated to the whole prop2 where l and r are
   two Prop, namely two statements that establish the equality 
   between two elements of the (carrier) of a setoid *)
notation "l ‡ r" 
   with precedence 90 for @{'prop2 $l $r }. 
interpretation "prop2" 
  'prop2 l r = (prop2 ???????? l r).
(* Notation A:setoid × B:setoid ⇒ C:setoid 
   associated to the whole structure binary_morphism *)
notation "A × term 74 B ⇒ term 19 C" 
   non associative with precedence 72 
   for @{'binary_morphism $A $B $C}.
interpretation "'binary_morphism0" 
   'binary_morphism A B C = (binary_morphism A B C).
(* Notation that abbreviates the statement "is reflexive"
   relatively to an equivalence relation of a setoid *)
notation "#" 
   with precedence 90 for @{'refl}. (**)
interpretation "refl" 'refl = (refl ???).

definition if: ∀A,B. (A \liff B) → A → B. 
(* CSC's original proof: intros; cases H; autobatch. *)
(* LR's "alternative" one to learn: *)
  #P1 #P2 #IFF whd in IFF; elim IFF #IF1 #IF2 @IF1 qed. 

definition fi: ∀A,B. (A \liff B) → B → A.
  #P1 #P2 #IFF whd in IFF; elim IFF #IF1 #IF2 @IF2 qed.

(* LR: The definition of PROP is an "exercise" that allows to formalize
       the idea that the set Prop of proposition in Matita together
       with the bi-implication Iff, which is an equivalence relation
       among p∈Prop form a setoid.
       
       Specifically, PROP is such that: *)
definition PROP: setoid.
  %
  [ @Prop (* the carrier of PROP is the set of propositions *)
  | %  (* the equivalence relation is *)
     [ @iff   (* the bi-implication that holds on Prop, 
                      which is defined in "logic/coimplication.ma" and
                      which we can prove to be: *)
     | #P1 % [ #P assumption | #P assumption] (* reflexive *)
     | #P1 #P2 #IFF cases IFF #IF1 #IF2 % [ @IF2 | @IF1] (* symmetric *)
     | #P1 #P2 #P3 #IFF1 #IFF2 cases IFF1 cases IFF2 #IF1 #IF2 #IF3 #IF4 %
       [ #P  @IF1 @IF3 | #P @IF4 @IF2 ]assumption 
      (* transitive *)
  ]] qed.

definition fi': ∀A,B:PROP. A=B → B → A ≝ fi.

notation ". r" 
   with precedence 50 for @{'fi $r}.
interpretation "fi" 
  'fi r = (fi' ?? r).

definition and_morphism: PROP × PROP ⇒ PROP.
 %
  [ @And (* LR: It's a bit obscure the reason why 
                     And: Prop → Prop → Prop  can be used here
                     where PROP → PROP → PROP is required *)
  | #P1 #P2 #P3 #P4 #Eq1 #Eq2 % #And %  elim Eq1 in And;
    [ #IF1 #IF2 * #P #PP @IF1 assumption
    | #IF1 #IF2 * #P #PP lapply Eq2 * #IF3 #IF4 @IF3 @PP
    | #IF1 #IF2 * #P #PP lapply Eq1 * #IF3 #IF4 @IF4 @P
    | #IF1 #IF2 * #P #PP lapply Eq2 * #IF3 #IF4 @IF4 @PP 
  ]
  ]
  
qed.

interpretation "and_morphism" 
  'and a b = (fun2 ??? and_morphism a b).

definition or_morphism: PROP × PROP ⇒ PROP.
 %[
    @Or
  | #P1 #P2 #P3 #P4 * #IF1 #IF2 * #IF3 #IF4 % [ * [ #PP % 1 @IF1 @PP | #PP % 2 @IF3 @PP]
  | * #PP [ % 1 @IF2 @PP | % 2 @IF4 @PP]]
  ] qed.

interpretation "or_morphism" 
  'or a b = (fun2 ??? or_morphism a b).

definition if_morphism: PROP × PROP ⇒ PROP.
 %
  [ @(λA,B. A → B)
  | normalize #P1 #P2 #P3 #P4 * #IF1 #IF2 * #IF3 #IF4 % #IF5 #PP [ @IF3 @IF5 @IF2 @PP | @IF4 @IF5 @IF1 @PP]
  ] qed.

(* LR: Added by me just as a curiosity. *)
interpretation "if_morphism" 
  'if a b = (fun2 ??? if_morphism a b).

